\begin{tabbing}
ecl{-}add{-}catch($A$; $l$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$spreadn(\=$A$;\+
\\[0ex]${\it Ta}$,${\it ksa}$,${\it ia}$,${\it ga}$,${\it ha}$,${\it aa}$,${\it ea}$.$<$${\it Ta}$
\\[0ex], ${\it ksa}$
\\[0ex], ${\it ia}$
\\[0ex], ${\it ga}$
\\[0ex], $\lambda$$n$,$x$. bor(\=band(($\neg_{b}$deq{-}member(nat{-}deq; $n$; $l$)); (${\it ha}$($n$,$x$)));\+
\\[0ex]band(($n$ =$_{0}$ 0); reduce(($\lambda$$m$,$b$. bor((${\it ha}$($m$,$x$)); $b$)); ff; $l$)))
\-\\[0ex], ${\it aa}$
\\[0ex], list{-}diff(nat{-}deq; ${\it ea}$; $l$)$>$)
\-
\end{tabbing}